Inference at * 1 2 
Iof proof for Lemma adjacent-cons:



1. T : Type
2. x : T
3. y : T
4. u : T
5. L : T List
6. i : {0..((||L||+1) - 1)}
7. x = [u / L][i]
8. y = [u / L][(i+1)]
9. 0 < ||L||
10. (i = 0)
  (x = u & y = hd(L))  (i:{0..(||L|| - 1)}. (x = L[i] & y = L[(i+1)])) 

latex

 by ((((OrRight) 
CollapseTHEN (Auto))) 
CollapseTHEN (((InstConcl [i - 1]) 
CollapseTHEN (
CAuto')))) 

latex

C1: 

C1:   x = L[(i - 1)]
C2: 

C2:   y = L[((i - 1)+1)]
C.

Definitions	n - m, #$n, P  Q, {T}, x:A. B(x), , Void, i  j < k, False, -n, i  j , [car / cdr], P & Q, x:A  B(x), , {x:A| B(x)} , , l[i], x:A. B(x), P  Q, x:AB(x), t  T, A  B, n+m, ||as||, A, s = t, {i..j}, type List, Type, a < b
Lemmas	int seg wf, nat wf, member wf, le wf, select wf